﻿module CoreEx
(* module CoreEx is used for extending the Core language AST with a context-graph "attached" to each node.
   It is used in the abstract-interpreter algorithm to hold the partial / temporary and eventually final interpretation 
   result graphs of each of the AST nodes analysis. *)
open BJK

(* datatype used for defining the AST extended with context-graph "attached" to each node. *)
type CmdEx = Skip | Asgn of int * Core.Expr | Choice of Cmd * Cmd | Seq  of Cmd * Cmd  | Loop of int * Cmd

and Cmd = | AICmd of CmdEx * (CG.graph ref) * int (* Constructor for a command with a graph "attached" and an identifier. *)
          | NaiveCmd of CmdEx * int               (* Constructor for a command with an identifier. *)
          | PolyCompCmd of CmdEx * int               (* Constructor for a command with an identifier. *)

    
(* this function raises an exception if the given AST contains an assignment command
    of the form Xi := e inside a loop whose counter variable is Xi, s.t. e <> Xi. *)      
let rec verifyLoopVarsUnmodifiedInsideLoopBodies(c : Core.Cmd) =
    let raiseLoopVarModifiedException(i) =
        Util.fail("Loop variable '" + BJKParse.parserLastVarToIndexMap().[i].ToString() + "' modified inside loop body.")

    let rec verifyVarUnmodifiedByCmd(i : int, c' : Core.Cmd) = 
        match c' with
        | Core.Asgn(i',e) ->
            if i = i' then 
                match e with
                | Core.Var x ->
                    if x <> i then raiseLoopVarModifiedException(i)
                    else ()
                | _ -> raiseLoopVarModifiedException(i)
            else ()
        | Core.Choice(c1,c2)  -> (verifyVarUnmodifiedByCmd(i,c1);verifyVarUnmodifiedByCmd(i,c2))
        | Core.Seq(c1,c2)     -> (verifyVarUnmodifiedByCmd(i,c1);verifyVarUnmodifiedByCmd(i,c2))
        | Core.Loop(i',c)     -> (verifyVarUnmodifiedByCmd(i,c);verifyVarUnmodifiedByCmd(i',c))
        | _ -> ()
            
    match c with
        | Core.Loop(i,c)     -> verifyVarUnmodifiedByCmd(i,c)
        | Core.Seq(c1,c2)    -> (verifyLoopVarsUnmodifiedInsideLoopBodies(c1);
                                    verifyLoopVarsUnmodifiedInsideLoopBodies(c2))
        | Core.Choice(c1,c2) -> (verifyLoopVarsUnmodifiedInsideLoopBodies(c1);
                                    verifyLoopVarsUnmodifiedInsideLoopBodies(c2))
        | _ -> ()
   
(* converts a regular AST to an extended AST ready for the Abstract Interpreter algorithm.
    Note:  loop body command c is expanded to: "if { c } else { Skip }".
    This is done to avoid calculating the Skip graph explicitly by the abstact interpreter algorithm. *)
let rec extendedAbsIntAST(c) =  
    let j = ref 0      
    let rec extAST = function
        | (Core.Skip)-> AICmd(Skip, ref (CG.newGraph([])),!j)
        | (Core.Asgn(i,e))     -> AICmd(Asgn(i,e), ref (CG.newGraph([])),!j)
        | (Core.Choice(c1,c2)) -> AICmd(Choice(extAST'(c1), extAST'(c2)), ref (CG.newGraph([])),!j)
        | (Core.Seq(c1,c2))    -> AICmd(Seq(extAST'(c1), extAST'(c2)), ref (CG.newGraph([])),!j)
        | (Core.Loop(i,c))     -> AICmd(Loop(i, extAST'(Core.Choice(Core.Skip,c))), ref (CG.newGraph([])),!j);   
    and extAST'(c) =
        let c' = extAST(c)
        let () = j := !j + 1
        c'
    let () = verifyLoopVarsUnmodifiedInsideLoopBodies(c)
    extAST'(c)

(* converts a regular AST to an extended AST ready for the naive analysis algorithm. *)
let rec extendedNaiveAST(c) =  
    let j = ref 0      
    let rec extAST = function
        | (Core.Skip)-> NaiveCmd(Skip, !j)
        | (Core.Asgn(i,e))     -> NaiveCmd(Asgn(i,e), !j)
        | (Core.Choice(c1,c2)) -> NaiveCmd(Choice(extAST'(c1), extAST'(c2)), !j)
        | (Core.Seq(c1,c2))    -> NaiveCmd(Seq(extAST'(c1), extAST'(c2)), !j)
        | (Core.Loop(i,c))     -> NaiveCmd(Loop(i, extAST'(c)), !j);   
    and extAST'(c) =
        let c' = extAST(c)
        let () = j := !j + 1
        c'
    let () = verifyLoopVarsUnmodifiedInsideLoopBodies(c)
    extAST'(c)
         

(* converts a regular AST to an extended AST ready for the PolyComp analysis algorithm. *)
let rec extendedPolyCompAST(c) =  
    let j = ref 0      
    let rec extAST = function
        | (Core.Skip)          -> PolyCompCmd(Skip, !j)
        | (Core.Asgn(i,e))     -> PolyCompCmd(Asgn(i,e), !j)
        | (Core.Choice(c1,c2)) -> PolyCompCmd(Choice(extAST'(c1), extAST'(c2)), !j)
        | (Core.Seq(c1,c2))    -> PolyCompCmd(Seq(extAST'(c1), extAST'(c2)), !j)
        | (Core.Loop(i,c))     -> PolyCompCmd(Loop(i, extAST'(c)), !j);   
    and extAST'(c) =
        let c' = extAST(c)
        let () = j := !j + 1
        c'
    let () = verifyLoopVarsUnmodifiedInsideLoopBodies(c)
    extAST'(c)
            
(* converts an extended AST to a regular AST. This letction is not the inverse of the extendedAST letction (due to the loop expansion). *)
let rec reducedAST = function
    | (AICmd(Skip, _,_))         -> Core.Skip
    | (AICmd(Asgn(i,e),_,_))     -> Core.Asgn(i,e)
    | (AICmd(Choice(c1,c2),_,_)) -> Core.Choice(reducedAST(c1),reducedAST(c2))
    | (AICmd(Seq(c1,c2),_,_))    -> Core.Seq(reducedAST(c1),reducedAST(c2))
    | (AICmd(Loop(i,c),_,_))     -> Core.Loop(i,reducedAST(c))
    | (NaiveCmd(Skip, _))         -> Core.Skip
    | (NaiveCmd(Asgn(i,e),_))     -> Core.Asgn(i,e)
    | (NaiveCmd(Choice(c1,c2),_)) -> Core.Choice(reducedAST(c1),reducedAST(c2))
    | (NaiveCmd(Seq(c1,c2),_))    -> Core.Seq(reducedAST(c1),reducedAST(c2))
    | (NaiveCmd(Loop(i,c),_))     -> Core.Loop(i,reducedAST(c))
    | (PolyCompCmd(Skip, _))         -> Core.Skip
    | (PolyCompCmd(Asgn(i,e), _))     -> Core.Asgn(i,e)
    | (PolyCompCmd(Choice(c1,c2), _)) -> Core.Choice(reducedAST(c1),reducedAST(c2))
    | (PolyCompCmd(Seq(c1,c2), _))    -> Core.Seq(reducedAST(c1),reducedAST(c2))
    | (PolyCompCmd(Loop(i,c), _))     -> Core.Loop(i,reducedAST(c));

(* extracts the graph of a CoreEx.Cmd *)
let graph = function
    | (AICmd(_,g,_)) -> g   
    | (NaiveCmd(_,_)) -> ref (CG.newGraph([]))     
    | (PolyCompCmd(_))   -> ref (CG.newGraph([]));

let pat = function
    | AICmd(Skip,_,_) -> Pattern.Skip
    | AICmd(_,_,id)  -> Pattern.Cmd(id) 
    | NaiveCmd(Skip,_) -> Pattern.Skip
    | NaiveCmd(_,id) -> Pattern.Cmd(id)
    | PolyCompCmd(Skip,_) -> Pattern.Skip
    | PolyCompCmd(_,id) -> Pattern.Cmd(id);
    
let id = function
         | (AICmd(_,_,id')) -> id'
         | (NaiveCmd(_,id')) -> id'
         | (PolyCompCmd(_,id)) -> 0;

(* prints the reduced AST of c *)
let prt(c) = Core.prt(reducedAST(c));  
